#include <stdio.h>
#include <math.h>
#include <stdlib.h>
#include <string.h>
#include "dcdflib.H"



int T = 100;




int main(int argc, char *argv[])
{

  //ALPHA BETA P0 P1 and BayesFactor definitions
  float ALPHA, BETA, P0, P1, BF;

  int i,j;
	
  //sucess and failure for the case of Walds algorithm and the Bayes Algorithm
  int success = 0;
  int failure = 0;
  int bsuccess = 0;
  int bfailure = 0;

  //output returned by the trace verification algorithm
  int out = -1;
	
  
  //file of the input model is called tcr_tomek%d.bngl where %d is count
  //input LTL file is called test%d.ltl where %d is countltl
  int count = 0, countltl = 0 ;
 

  char scount[100];
  char cmd[1000];
  char modelfile[1000];
  char ltlfile[1000];
  char numvar[1000];
  char lentrace[1000];
	
  //has a decision been reached yet?
  float decision = 0;
  float bayesdecision = 0;

  //was the wald's or bayes test complete
  int walddone=0;
  int bayesdone=0;

  //numerator being computes
  //bayes result being computed
  double nr=0;
  double bayesresult=0;


  /*beta function computation parameters with initial values*/
  int which = 1;
  double p = 0;
  double q = 0;
  double x = 0.4;
  double y = 1-x;
  double a = 20;
  double b = 10;
  int status = 1;
  double bound = 0;
  double betacdf=0;


  FILE *fptestsuite;

  /*These lines test that the cdfbet library is producing correct results */
    cdfbet ( &which, &p, &q, &x, &y,  &a, &b, &status, &bound );
  //  printf ("%f %f\n",p,q);
	

 //Test Suite of Input Models and LTL Properties

    /*
  fptestsuite = fopen("testsuite","r");
  
  if (fptestsuite==NULL) 
    {
      printf("Test Suite File Not Present\n");
      exit(-1);
    }
    */
  /***********************************************/


    //compile the LTL translator

    printf("\n\nPlease wait...Assuring integrity of the Statistical Model Checker\n\n");
  system("./run >& logfile.compile");
	
  printf("\n\n BioLAB Statistical Model Checker\n Developed by Edmund Clarke, Sumit Kumar Jha, Christopher Langmead, James Faeder\n Carnegie Mellon University\n\n\n\n Correct Usage: ./smc modelfile ltlfile ALPHA BETA P0 P1 number_of_variables_in_data_file, number_of_simulation_points_to_be_analyzed\n");


	  
      walddone=0;
      bayesdone=0;

      count++;

      //      fscanf(fptestsuite, "%d %d %f %f %f %f %f ", &count, &countltl, &ALPHA, &BETA, &P0, &P1, &BF  );

      

      
      strcpy(modelfile,argv[1]);
      strcpy(ltlfile,argv[2]);
      ALPHA = strtod(argv[3],NULL);
      BETA = strtod(argv[4],NULL);
      P0 = strtod(argv[5],NULL);
      P1 = strtod(argv[6],NULL);
      strcpy(numvar,argv[7]);
      strcpy(lentrace,argv[8]);


      //printf("\naa%s %saa %d\n",argv[1],modelfile,argc);
      //exit(-1);

      sprintf(cmd,"rm -rf result%s_%s\n",modelfile,ltlfile);
      system(cmd);
     
      while(1)
	{




	  //sprintf(scount,"%d",count);
	  sprintf(cmd,"./bionetgen/BioNetGen_2.0.46/Perl2/BNG2.pl ./bionetgen/BioNetGen_2.0.46/Models2/%s.bngl\n", modelfile);
	  printf("\n%s\n",cmd);
	  out = system(cmd); 
	
	  if(out<0) exit(-1);



	  sprintf(cmd,"cp -rf ./bionetgen/BioNetGen_2.0.46/Models2/%s_ssa.gdat ./data.txt\n", modelfile);	
	  printf("\n%s\n",cmd);
	  out = system(cmd);

	  if(out<0) exit(-1);

	  sprintf(cmd,"sed -i  \'1i %s %s\' data.txt\n", numvar, lentrace);
	  printf("\n%s\n",cmd);
	  out = system(cmd);
	  if(out<0) exit(-1); 


	  sprintf(cmd,"./a.out \"data.txt\" < %s\n",ltlfile);
	  printf("\n%s\n",cmd);
	  out = system(cmd);
	  if(out<0) exit(-1);
	
	  if (out!=0 || out !=1)
	    {
	      //probably a value of avrage time spent
	      if (out>=T) 
		out=1;
	      else
		out=0;	
	    }

	  if (out==0) 
	    failure++;
	  else
	    success++;
	



	  /*Wald's Decision Algorithm*/

	  decision = success * log (P1/P0) + failure * log ( (1-P1)/(1-P0));
	  printf("Success %d Failure %d\n", success, failure); 
	
	  if (walddone==0 && decision <= log (BETA/(1-ALPHA)) )
	    {
	      printf("Property Satisfied"); 

	      sprintf(cmd,"echo  \"Satisfied Success %d Failure %d \" > result%s_%s\n ",modelfile,ltlfile);
	      printf("\n%s\n",cmd);
	      system(cmd);
	      walddone=1;
	    }
	
	  if (walddone==0 && decision >= log ((1-BETA)/ALPHA) )
	    {
	      printf("Property NOT Satisfied"); 
	      sprintf(cmd,"echo  \"NOT Satisfied Success %d Failure %d\" > result%s_%s\n ",modelfile,ltlfile);
	      printf("\n%s\n",cmd);
	      system(cmd);
	      walddone=1;
	    }
	

	  /*
	  //Bayesian Decision Algorithm
	  which=1; p=-1; q=-1; a=success+1; b=failure+1;

	  x=P0; y = 1-P0;
	  cdfbet ( &which, &p, &q, &x, &y, &a, &b, &status, &bound );
	  nr = p;

	  bayesdecision = (p/(1-p))*((1-P0)/P0);


	  if (bayesdone ==0  && bayesdecision >= BF )
	    {
	      printf("Property Satisfied"); 
	      sprintf(cmd,"rm -rf bayesresult%d_%d_%f\n",count, countltl, P0);
	      system(cmd);
	      sprintf(cmd,"echo  \"Satisfied Success %d Failure %d bayesresult %f \" > bayesresult%d_%d_%f\n ",success, failure, bayesresult, count,countltl, P0);
	      system(cmd);
	      bayesdone=1;
	    }
	
	  if (bayesdone ==0  && bayesdecision <= 1/BF )
	    {
	      printf("Property NOT Satisfied"); 
	      sprintf(cmd,"rm -rf bayesresult%d_%d_%f\n",count,countltl,P0);
	      system(cmd);
	      sprintf(cmd,"echo  \"NOT Satisfied Success %d Failure %dbayesresult %f \" > bayesresult%d_%d_%f\n ",success, failure,  bayesresult, count,countltl, P0);
	      system(cmd);
	      bayesdone=1;
	    }
	

	  */

	  bayesdone=1; //comment this out later
	  if (walddone==1&&bayesdone==1) break;

	}
	

      success=0;
      failure=0;
      decision = 0;
      bayesdecision = 0;

}
		
	

